/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

/** BLPSolverMessage: a class that represents a message from
    PSolver. there are several types of message and for each
    type there are additional fields to represent additional information
    sent in that message. The rep of this class is basically a union
    - depending on the type of message, certain fields are used and
    others are not.
*/

public class BLPSolverMessage {
    // constants for different types of messages
    private static final int STATUS = 0;
    private static final int ACK = 1;
    private static final int PROGRESS = 2;
    private static final int SOLUTION = 3;
    private static final int CANCELLED = 4;
    private static final int TIMEOUT = 5;
    private static final int INVALID = 6;
    private static final int BLANK = 7;

    // constants for solution types
    public static final int UNSAT = 0;
    public static final int SAT = 1;


    // field to hold type
    private int _myType;

    // additional fields - different ones are actually used for diffent type
    // of messags

    // status fields
    private String _statusMessage;

    // ack fields
    private int _clientId;

    // progress fields
    private int _progressVal;

    // solution fields
    private int _solutionType;

    // testers for the different type of messages

    public boolean isStatus () { return _myType == STATUS; }
    public boolean isAcknowledged () { return _myType == ACK; }
    public boolean isProgress () { return _myType == PROGRESS; }
    public boolean isSolution () { return _myType == SOLUTION; }
    public boolean isTimeout () { return _myType == TIMEOUT; }
    public boolean isCancelled () { return _myType == CANCELLED; }
    public boolean isBlank () { return _myType == BLANK; }

    // accessors for fields
    // of course if they're used on the wrong type of message, values are
    // undefined

    public String getStatusMessage () { return _statusMessage; }
    public int getClientId () { return _clientId; }
    public int getProgressValue () { return _progressVal; }
    public int getSolutionType () { return _solutionType; }

    public BLPSolverMessage (String messageString) {
    // constructor - takes the string with the message
    // and interprets it appropriately

    // check if it's a status message
    if (messageString.indexOf ("server_status") != -1) {
        _myType = STATUS;
        String afterStatus = messageString.substring (messageString.indexOf ("default") + 9);
        _statusMessage = afterStatus.substring (0, afterStatus.indexOf (">"));
    }

    // a progress message ?
    else if (messageString.indexOf ("server_progress") != -1) {
        _myType = PROGRESS;
        String afterProgress = messageString.substring (messageString.indexOf ("default") + 8);
        _progressVal = Integer.valueOf (afterProgress.substring (0, afterProgress.indexOf (">")).trim ()).intValue ();
    }

    // an ack message ?
    else if (messageString.indexOf ("server_user_ack") != -1) {
        _myType = ACK;
        String afterAck = messageString.substring (messageString.indexOf ("clientId") + 8);
        //System.out.println ("afterAck: " + afterAck);
        String cidString  = afterAck.substring (0, afterAck.indexOf (">"));
        //System.out.println ("cidString: " + cidString);
        _clientId = Integer.valueOf (cidString.trim ()).intValue ();
    }

    else if (messageString.indexOf ("server_result") != -1) {
        // could be a sol, cancelled, or timeout
        String afterResult = messageString.substring (messageString.indexOf ("default") + 9);
        String resultCodeString = afterResult.substring (0, afterResult.indexOf ("<"));
        int resultCode = Integer.valueOf (resultCodeString.trim ()).intValue ();
        if (resultCode == 0 || resultCode == 1) {
        _myType = SOLUTION;
        _solutionType = resultCode == 0 ? SAT : UNSAT;
        }
        else if (resultCode == 2)
        _myType = TIMEOUT;
        else if (resultCode == 3)
        _myType = CANCELLED;
        else
        _myType = INVALID;
    }
    else
        _myType = INVALID;
    }

    public BLPSolverMessage () { _myType = BLANK; }
}
